Lôgic BAN (tiếng Anh: BAN logic, viết tắt của Burrows-Abadi-Needham logic) là một tập hợp các quy tắc để định nghĩa và phân tích các giao thức truyền thông. Cụ thể hơn, lôgic BAN được dùng để kiểm tra các giao thức có đảm bảo an toàn trước những kẻ tấn công hay không. Trong lôgic BAN, người ta giả định các giao dịch được thực hiện trên một môi trường không an toàn và kẻ tấn công luôn có khả năng đọc được các gói tin trên đường truyền. Điều này được phát triển thành một nguyên tắc trong an ninh hệ thống: "Không được tin vào mạng truyền dẫn".Tên của lôgic BAN được đặt theo tên của 3 nhà khoa học đã tạo ra nó: Michael Burrows, Martín Abadi, và Roger Needham.Một quy trình sử dụng lôgic BAN tiêu biểu bao gồm 3 bước:[1]Để phân tích các giao thức, lôgic BAN sử dụng các định đề và định nghĩa. Trước khi đưa vào phân tích, các giao thức cần được biểu diễn theo hệ thống ký hiệu giao thức mật mã (cách biểu diễn này thường có trong các bài nghiên cứu).